We have annual competitions in this. It's getting quite tough nowadays. So we have big

benchmarks that basically come from this idea. If I have an NP-complete problem, then I find

a clever way of translating it into propositional logic. Then you get these kind of datasets that

have a million clauses, which we then feed to a clause, to a satisfiability checker.

They can usually deal with them. You could do local search, but kind of local search

techniques have plateaued, and via tricks like clause learning, DPLL hasn't really.

So we're seeing that. There's a huge realm of doing efficient implementations of unit propagation.

Turns out that just by doing clever implementation tricks, there's a technique called binary

decision diagrams, BDDs. You can get things like three orders of magnitude of efficiency,

which really makes a difference. This is still active. Most of the people working there would

not consider themselves as AI researchers, but either theoretical computer scientists or

engineers. Again, this is largely solved. We know what we're doing. We can let the engineer join

the fun, but it's an original AI technique. You can imagine that there's lots of stuff,

because lots of clever people are doing things there. Any questions about this?